\begin{tabbing}
$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), $L_{1}$, $L_{2}$:($T$ List).
\\[0ex]no\_repeats($T$;$L_{1}$)
\\[0ex]$\Rightarrow$ \=(($\forall$$x$:$T$. ($x$ $\in$ $L_{2}$) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ $L_{1}$) \& ($\uparrow$($P$($x$)))))\+
\\[0ex]\& ($\forall$$x$, $y$:$T$. $x$ before $y$ $\in$ $L_{2}$ $\Rightarrow$ $x$ before $y$ $\in$ $L_{1}$))
\-\\[0ex]$\Rightarrow$ (filter($P$;$L_{1}$) = $L_{2}$)
\end{tabbing}